($\lambda$$E$,$x$,$y$,$z$. tree\_node($<$$x$, $y$$>$)) $\in$ $E$:Type$\rightarrow$Tree($E$)$\rightarrow$Tree($E$)$\rightarrow\downarrow$True$\rightarrow$Tree($E$)